(set-option :proof true)
(declare-sort a$) 
(declare-sort c$) 
(declare-sort d$) 
(declare-sort f$) 
(declare-sort e$)      
(declare-fun comp$b ( f$ ) e$) 
(declare-fun m$g ( e$ d$ ) f$)  
(declare-fun m$ac ( f$ a$ ) c$) (declare-fun m$aw ( d$ a$ ) a$)   
(assert (forall (( ?h f$ ) ( ?i d$ ) ( ?j f$ ) ( ?k d$ )) 
    (= (= (m$g (comp$b ?h) ?i) (m$g (comp$b ?j) ?k)) 
        (forall (( ?l a$ )) (= (m$ac ?h (m$aw ?i ?l )) (m$ac ?j (m$aw ?k ?l )))) false)))  
(check-sat)